T:Type, as, bs:T List, b:T. as = (as @ (b.bs))  False 

latex

Definitions	t  T, False, x:A. B(x), Prop, P  Q, P  Q, P & Q, P  Q, as @ bs, Top, S  T, ||as||, A, P  Q, Dec(P)
Lemmas	decidable false, append-cancellation, length wf1, append nil sq, top wf, append wf, false wf